Nuprl Lemma : comb_for_int_seg_wf
13,42
postcript
pdf
(
m
,
n
,
z
. {
m
..
n
})
(
True)
Type
latex
Up
int
1
,
int
1
Definitions
t
T
,
,
x
:
A
.
B
(
x
)
,
T
Lemmas
true
wf
,
squash
wf
,
int
seg
wf
origin
m,n,z. {m..n
}) 
(
True)Type m,n,z. {m..n}) (True)Type T
x:A. B(x)T